↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
SLOWSORT_IN_AG(X, Y) → U1_AG(X, Y, perm_in_ag(X, Y))
SLOWSORT_IN_AG(X, Y) → PERM_IN_AG(X, Y)
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_GAA(U, .(X, Y), Z)
DELETE_IN_GAA(X, .(Y, Z), W) → U7_GAA(X, Y, Z, W, delete_in_gaa(X, Z, W))
DELETE_IN_GAA(X, .(Y, Z), W) → DELETE_IN_GAA(X, Z, W)
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_AG(X, Y, U, V, perm_in_ag(Z, V))
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → PERM_IN_AG(Z, V)
U1_AG(X, Y, perm_out_ag(X, Y)) → U2_AG(X, Y, sorted_in_g(Y))
U1_AG(X, Y, perm_out_ag(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → U8_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U3_G(X, Y, Z, le_out_gg(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
SLOWSORT_IN_AG(X, Y) → U1_AG(X, Y, perm_in_ag(X, Y))
SLOWSORT_IN_AG(X, Y) → PERM_IN_AG(X, Y)
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_GAA(U, .(X, Y), Z)
DELETE_IN_GAA(X, .(Y, Z), W) → U7_GAA(X, Y, Z, W, delete_in_gaa(X, Z, W))
DELETE_IN_GAA(X, .(Y, Z), W) → DELETE_IN_GAA(X, Z, W)
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_AG(X, Y, U, V, perm_in_ag(Z, V))
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → PERM_IN_AG(Z, V)
U1_AG(X, Y, perm_out_ag(X, Y)) → U2_AG(X, Y, sorted_in_g(Y))
U1_AG(X, Y, perm_out_ag(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → U8_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U3_G(X, Y, Z, le_out_gg(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(Y, Z, le_in_gg(X, Y))
U3_G(Y, Z, le_out_gg) → SORTED_IN_G(.(Y, Z))
le_in_gg(s(X), s(Y)) → U8_gg(le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg
le_in_gg(0, 0) → le_out_gg
U8_gg(le_out_gg) → le_out_gg
le_in_gg(x0, x1)
U8_gg(x0)
The following rules are removed from R:
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(Y, Z, le_in_gg(X, Y))
U3_G(Y, Z, le_out_gg) → SORTED_IN_G(.(Y, Z))
Used ordering: POLO with Polynomial interpretation [25]:
le_in_gg(s(X), s(Y)) → U8_gg(le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg
le_in_gg(0, 0) → le_out_gg
U8_gg(le_out_gg) → le_out_gg
POL(.(x1, x2)) = 2 + 2·x1 + 2·x2
POL(0) = 1
POL(SORTED_IN_G(x1)) = 1 + x1
POL(U3_G(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3
POL(U8_gg(x1)) = 2 + x1
POL(le_in_gg(x1, x2)) = x1 + x2
POL(le_out_gg) = 2
POL(s(x1)) = 1 + 2·x1
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
le_in_gg(x0, x1)
U8_gg(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
DELETE_IN_GAA(X, .(Y, Z), W) → DELETE_IN_GAA(X, Z, W)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
DELETE_IN_GAA(X, .(Y, Z), W) → DELETE_IN_GAA(X, Z, W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PrologToPiTRSProof
DELETE_IN_GAA(X) → DELETE_IN_GAA(X)
DELETE_IN_GAA(X) → DELETE_IN_GAA(X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → PERM_IN_AG(Z, V)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → PERM_IN_AG(Z, V)
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PrologToPiTRSProof
U5_AG(V, delete_out_gaa) → PERM_IN_AG(V)
PERM_IN_AG(.(U, .(V, []))) → U5_AG(V, delete_in_gaa(U))
delete_in_gaa(X) → delete_out_gaa
delete_in_gaa(X) → U7_gaa(delete_in_gaa(X))
U7_gaa(delete_out_gaa) → delete_out_gaa
delete_in_gaa(x0)
U7_gaa(x0)
From the DPs we obtained the following set of size-change graphs:
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
SLOWSORT_IN_AG(X, Y) → U1_AG(X, Y, perm_in_ag(X, Y))
SLOWSORT_IN_AG(X, Y) → PERM_IN_AG(X, Y)
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_GAA(U, .(X, Y), Z)
DELETE_IN_GAA(X, .(Y, Z), W) → U7_GAA(X, Y, Z, W, delete_in_gaa(X, Z, W))
DELETE_IN_GAA(X, .(Y, Z), W) → DELETE_IN_GAA(X, Z, W)
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_AG(X, Y, U, V, perm_in_ag(Z, V))
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → PERM_IN_AG(Z, V)
U1_AG(X, Y, perm_out_ag(X, Y)) → U2_AG(X, Y, sorted_in_g(Y))
U1_AG(X, Y, perm_out_ag(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → U8_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U3_G(X, Y, Z, le_out_gg(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
SLOWSORT_IN_AG(X, Y) → U1_AG(X, Y, perm_in_ag(X, Y))
SLOWSORT_IN_AG(X, Y) → PERM_IN_AG(X, Y)
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_GAA(U, .(X, Y), Z)
DELETE_IN_GAA(X, .(Y, Z), W) → U7_GAA(X, Y, Z, W, delete_in_gaa(X, Z, W))
DELETE_IN_GAA(X, .(Y, Z), W) → DELETE_IN_GAA(X, Z, W)
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_AG(X, Y, U, V, perm_in_ag(Z, V))
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → PERM_IN_AG(Z, V)
U1_AG(X, Y, perm_out_ag(X, Y)) → U2_AG(X, Y, sorted_in_g(Y))
U1_AG(X, Y, perm_out_ag(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → U8_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U3_G(X, Y, Z, le_out_gg(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ PiDP
↳ PiDP
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
le_in_gg(x0, x1)
U8_gg(x0, x1, x2)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
POL(.(x1, x2)) = 1 + 2·x1 + x2
POL(0) = 0
POL(SORTED_IN_G(x1)) = 2·x1
POL(U3_G(x1, x2, x3, x4)) = 2 + 2·x1 + 2·x2 + 2·x3 + x4
POL(U8_gg(x1, x2, x3)) = x1 + 2·x2 + x3
POL(le_in_gg(x1, x2)) = x1 + 2·x2
POL(le_out_gg(x1, x2)) = x1 + 2·x2
POL(s(x1)) = 2·x1
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
↳ PiDP
↳ PiDP
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
le_in_gg(x0, x1)
U8_gg(x0, x1, x2)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
DELETE_IN_GAA(X, .(Y, Z), W) → DELETE_IN_GAA(X, Z, W)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
DELETE_IN_GAA(X, .(Y, Z), W) → DELETE_IN_GAA(X, Z, W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
DELETE_IN_GAA(X) → DELETE_IN_GAA(X)
DELETE_IN_GAA(X) → DELETE_IN_GAA(X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → PERM_IN_AG(Z, V)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_ag(Z, V))
U6_ag(X, Y, U, V, perm_out_ag(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_gaa(U, .(X, Y), Z))
U5_AG(X, Y, U, V, delete_out_gaa(U, .(X, Y), Z)) → PERM_IN_AG(Z, V)
delete_in_gaa(X, .(X, Y), Y) → delete_out_gaa(X, .(X, Y), Y)
delete_in_gaa(X, .(Y, Z), W) → U7_gaa(X, Y, Z, W, delete_in_gaa(X, Z, W))
U7_gaa(X, Y, Z, W, delete_out_gaa(X, Z, W)) → delete_out_gaa(X, .(Y, Z), W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
U5_AG(U, V, delete_out_gaa(U)) → PERM_IN_AG(V)
PERM_IN_AG(.(U, .(V, []))) → U5_AG(U, V, delete_in_gaa(U))
delete_in_gaa(X) → delete_out_gaa(X)
delete_in_gaa(X) → U7_gaa(X, delete_in_gaa(X))
U7_gaa(X, delete_out_gaa(X)) → delete_out_gaa(X)
delete_in_gaa(x0)
U7_gaa(x0, x1)
From the DPs we obtained the following set of size-change graphs: